package at.fhj.ase;

import java.math.BigDecimal;
import java.util.ArrayList;
import java.util.Iterator;
import java.util.List;

//@ model import org.jmlspecs.models.*;


public class ShoppingCart {

	private /*@ spec_public @*/ long nextPosNr = 0;
	

	 private List<ShoppingCartPos> posList = new ArrayList<ShoppingCartPos>() ;	
	
	public ShoppingCart(){
		
	}
	
	/*@ public normal_behavior
	  @ 	requires article != null;
	  @		requires price != null && price.compareTo(new BigDecimal("0")) >= 0; // >= 0
	  @		requires quantity >= 0;
	  @		assignable \nothing;
	  @ also public exceptional_behavior
	  @		requires  article == null;
	  @		signals (NullPointerException);
	  @		also requires  price == null;
	  @		signals (NullPointerException);
	  @		also requires price.compareTo(new BigDecimal("0")) == -1; // < 0
	  @		signals (IllegalArgumentException);
	  @		also requires quantity <= 0;
	  @		signals (IllegalArgumentException);
	  @		assignable \nothing;
	  @*/
	public void addToCart(final Article article, final BigDecimal price, final long quantity) 
				throws NullPointerException, IllegalArgumentException {
		posList.add(new ShoppingCartPos(getNextPosNr(), article, price, quantity));
		this.nextPosNr++;
	}
	
	/*@ public normal_behavior 
	  @ 	requires pos != null;
	  @ 	requires !posList.isEmpty();
	  @ 	requires posList.contains(pos);
	  @		assignable \nothing;
	  @ ensures nextPosNr == \old(nextPosNr) - 1;
	  @ also public exceptional_behavior
	  @		requires pos == null;
	  @ 	signals (NullPointerException);
	  @		requires !posList.contains(pos);
	  @		signals (IllegalArgumentException);
	  @		assignable \nothing;
	  @*/
	public void removeFromCart(ShoppingCartPos pos) 
			throws IllegalArgumentException, NullPointerException {
		if(pos == null) {
			throw new NullPointerException("shoppingCartPos must not be null");
		}
		if(!posList.contains(pos)) {
			throw new IllegalArgumentException("wrong posNr");
		}
		posList.remove(pos);
		this.nextPosNr--;
	}
	
	//@ also ensures \result == posList;
	public List<ShoppingCartPos> getShoppingCartList() {
		return this.posList;
	}

	/*@ public normal_behavior 
	  @ 	requires posList != null; 
	  @ 	requires !posList.isEmpty();
	  @		assignable \nothing;
	  @ also public exceptional_behavior
	  @		requires posList == null;
	  @ 	signals (NullPointerException);
	  @		also requires posList.isEmpty();
	  @		signals(IllegalArgumentException);
	  @*/
	public BigDecimal getTotalSum() 
			throws NullPointerException, IllegalArgumentException {
		if(posList == null) {
			throw new NullPointerException("posList must not be null");
		}
		if(posList.isEmpty()) {
			throw new IllegalArgumentException("posList must not be empty");
		}
		BigDecimal sum = new BigDecimal("0");
		for (ShoppingCartPos p : posList) {
			sum = sum.add(p.getTotalPrice());
		}
			
		return sum;
	}
	
	//@ ensures \result == nextPosNr;
	protected final long getNextPosNr() {
		return this.nextPosNr;
	}
	
//	private final void setNextPosNr() {
//		this.nextPosNr ++;
//	}
	
	//@ also ensures \result != null;
	public String toString() {
		Iterator<ShoppingCartPos> articleIterator = posList.iterator();
		StringBuilder s = new StringBuilder();
		while(articleIterator.hasNext()) {
			s.append(articleIterator.next().toString()).append("\n");
		}
		return s.toString();
	}
	

}
